T:(IdType), tab:secret-table(T), kx:(:( + Atom1)  Atom1). decrypt(tab;kx)  (?data(T)) 

latex

Definitions	t  T, x:A. B(x), data(T), , inr x , ff, Unit, left + right, x:AB(x), , b, A, b, s = t, , inl x , Type, st-key-match(tab;k1;k2), if b then t else f fi , st-lookup(tab;x), Atom$n, , x:A  B(x), P  Q, outl(x), let x,y = A in B(x;y), isl(x), P & Q, P  Q, decrypt(tab;kval), Id, secret-table(T)
Lemmas	secret-table wf, Id wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, isl wf, outl wf, nat wf, st-lookup wf, ifthenelse wf, st-key-match wf, unit wf, bool wf, bnot wf, not wf, assert wf, bfalse wf, it wf, data wf